COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR t t1 t2 t3 t4 ε tower
C00004 ENDMK
C⊗;
declare INDVAR t t1 t2 t3 t4 ε tower;
declare INDVAR s s0 s1 s2 s3 ε situation;

declare PREDCONST movable(tower,tower,situation),on(tower,tower,situation);
declare PREDCONST reachable(situation,situation);
declare PREDPAR P 1;

axiom moveable:
	∀t1 t2 s.(movable(t1,t2,s) ⊃ ∃s1.(reachable(s,s1) ∧
		on(t1,t2,s1) ∧ ∀t3 t4.(¬(t3=t1) ⊃ (on(t3,t4,s1) ≡ on(t3,t4,s)))))
;;

declare OPCONST move(tower,tower,situation) = situation;

axiom move:
	∀t1 t2 s.(¬movable(t1,t2,s) ⊃ move(t1,t2,s) = s)
	∀t1 t2 s.(movable(t1,t2,s) ⊃ on(t1,t2,move(t1,t2,s)) ∧
		∀t3 t4.(¬(t3=t1) ⊃ on(t3,t4,move(t1,t2,s)) ≡ on(t3,t4,s)))
;;

axiom reachable:
	∀s.reachable(s,s)
	∀s1 s2 s3.(reachable(s1,s2) ∧ reachable(s2,s3) ⊃ reachable(s1,s3))
	∀s0.(P(s0) ∧ ∀s t1 t2.(P(s) ⊃ P(move(t1,t2,s)))
				⊃ ∀s.(reachable(s0,s) ⊃ P(s)))
;;